r, s:RngSig. RingHom(r;s)   

latex

Up	rings 1
Definitions of Statement	RingHom(R;S)
Definitions	P & Q, RingHom(R;S), , t  T, x:A. B(x)
Lemmas	rng sig wf, rng one wf, rng times wf, rng plus wf, fun thru 2op wf, rng car wf